Nuprl Lemma : d-O_wf
0,22
postcript
pdf
i
:Id. Outlnk(
i
)
IdLnk
Prop
latex
Definitions
Outlnk(
i
)
,
Prop
,
source(
l
)
,
x
:
A
.
B
(
x
)
,
IdLnk
,
t
T
,
Id
Lemmas
Id
wf
,
IdLnk
wf
,
lsrc
wf
origin
i:Id. Outlnk(i) 
IdLnk
Prop i:Id. Outlnk(i) IdLnkProp x:A. B(x) T